(set-logic QF_AX)
(set-info :status sat)
(declare-sort I 0)
(declare-sort E 0)
(declare-fun a () (Array I E))
(declare-fun b () (Array I E))
(declare-fun i () I)
(declare-fun j () I)
(declare-fun v () E)
(declare-fun w () E)
(declare-fun u () E)
(declare-fun x () Bool)

(assert (not (= i j)))
(assert (= (select a i) v))
(assert (= (select b i) u))
(assert (= (store a j w) b))
(assert (or (not x) (not (= (select a i) (select b i)))))
(check-sat)
